\begin{tabbing}
$\forall$$T$:Type, $i$:$\mathbb{N}$, $l$:$T$ List, $f$:(Top$\rightarrow$$T$$\rightarrow$Top), $y$:Top.
\\[0ex]$i$$<\parallel$$l$$\parallel$
\\[0ex]$\Rightarrow$ (\=list\_accum($x$,$a$.$f$($x$,$a$);$y$;$l$)\+
\\[0ex]$\sim$
\\[0ex]list\_accum($x$,$a$.$f$($x$,$a$);list\_accum($x$,$a$.$f$($x$,$a$);$y$;firstn($i$;$l$));nth\_tl($i$;$l$)))
\-
\end{tabbing}